package compilador.gerador.comando;

import static compilador.gerador.GeradorDeCodigo.INVARIANTE_SEM_NOME;
import compilador.Command;
import compilador.CommandException;
import compilador.gerador.ClasseCodigo;
import compilador.gerador.GeradorDeCodigo;

public class VerificaImpliesCommand implements Command {
	
	private static final String IMPLIES = "implies";

	private String condicao = null;
	private String consequence = null;
	private String extra = null;

	@Override
	public void run(String... args) throws CommandException {
		GeradorDeCodigo gerador = GeradorDeCodigo.getInstance();
		String buffer = gerador.getMarked();

		if (buffer.matches(".*"+IMPLIES+".*")) {
			processBuffer(buffer);

			ClasseCodigo codigo = gerador.getClasseCodigo();
			String invName = INVARIANTE_SEM_NOME + codigo.getNextInvNumber();
			String inv = createInvariante(invName, condicao, consequence);
			codigo.addInv(inv);
			gerador.removeMarked();
			gerador.appendCode("this." + invName + "()");
			if (extra != null) {
				gerador.appendCode(extra);
			}
		}
	}

	private void processBuffer(String buffer) {
		int impliesStart = buffer.indexOf(IMPLIES);
		int impliesEnd = buffer.indexOf(IMPLIES) + 7;
		char[] begin = buffer.substring(0, impliesStart).toCharArray();
		int parenteses = 0;
		for (char c : begin) {
			if (c == '(') {
				parenteses++;
			} else if (c == ')') {
				parenteses--;
			}
		}
		if (parenteses == 0) {
			condicao = buffer.substring(0, impliesStart);
			consequence = buffer.substring(impliesEnd);
		} else {
			int i = 0;
			do {
				if (begin[i] == '(')
					parenteses--;
				if (parenteses == 0)
					break;
				i++;
			} while (i < impliesStart);
			condicao = buffer.substring(i+1, impliesStart);			
			
			char[] end = buffer.substring(impliesEnd).toCharArray();
			parenteses = 0;
			int index = 0;
			do {
				char c = end[index];
				if (c == '(') {
					parenteses++;
				} else if (c == ')') {
					parenteses--;
				}
				index++;
			} while (parenteses >= 0);
			int indexParenteses = index + impliesEnd;
			consequence = buffer.substring(impliesEnd, indexParenteses-1);
			extra = buffer.substring(indexParenteses);
		}

	}

	private String createInvariante(String nextInvNumber, String condicao, String consequence) {
		return "\tboolean " + nextInvNumber + "(){\n\t\treturn (" + condicao + ")?" + consequence + ":false;\n\t}\n";
	}

}
